Nuprl Definition : ma-sframe 0,22

M.sframe(k sends <l,tg>)
== L != 1of(2of(2of(2of(2of(2of(2of(2of(M))))))))(<l,tg>)  deq-member(KindDeq;k;L
latex



clarification:

M.sframe(k sends <l,tg>)
== fpf-val(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);
== fpf-val(1of(2of(2of(2of(2of(2of(2of(2of(M))))))));
== fpf-val(<l,tg>;
== fpf-val(x,L.deq-member(KindDeq;k;L)) 
latex


DefinitionsM.sframe(k sends <l,tg>), z != f(x P(a;z), product-deq(A;B;a;b), IdLnk, Id, IdLnkDeq, IdDeq, 1of(t), 2of(t), b, deq-member(eq;x;L), KindDeq
FDL editor aliasesma-sframe

origin